w:World, e:E. FairFifo  w-info(w;e)  IdId+(IdLnkE)Id 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), kind(e), isrcv(k), left+right, P  Q, Dec(P), b, b, x:AB(x), x:AB(x), P & Q, P  Q, Id, tag(k), sender(e), lnk(k), <a,b>, inr(x), , s = t, Prop, E, IdLnk, act(k), loc(e), inl(x), islocal(k), Unit, kindcase(k; a.f(a); l,t.g(l;t) ), w-info(w;e), World, FairFifo
Lemmas	fair-fifo wf, world wf, eqtt to assert, iff transitivity, eqff to assert, islocal wf, w-loc wf, actof wf, IdLnk wf, w-E wf, bool wf, lnk wf, w-sender wf, tagof wf, Id wf, islocal-not-isrcv, not functionality wrt iff, assert of bnot, bnot wf, not wf, assert wf, decidable assert, isrcv wf, w-ekind wf